Step of Proof: inv_image_ind_tp 9,38
Inference at * 1 1 1 
Iof proof for Lemma inv image ind tp:



1. T : Type
2. r : TT
3. S : Type
4. f : ST
5. WellFnd{i}(T;x,y.r(x,y))
6. P : S
7. j:S. (k:S. r(f(k),f(j))  P(k))  P(j)
8. n : S
  P(n) 
latex
 by (PushArgs 
[`f`,term_to_arg f 
;`T`,term_to_arg T 
;`n`,var_to_arg `n' 
;`nn`,var_to_arg `nn' 

;`;`S`,term_to_arg S 
;`i`,int_to_arg 8 
;`RangeIndTac`, tactic_text_to_arg (
;`itext_term "(WFndHypInd 5 (-1))") 
]) 
latex

])1: 

])1:   P(n)
]).

origin